\begin{tabbing}
$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$).
\\[0ex]Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal(${\it da}$)
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$ecl{-}kinds($A$). (isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)) $\in$ Id) \& $k$ $\in$ dom(${\it da}$))
\\[0ex]$\Rightarrow$ $\neg$"ecl" $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ \=ecl{-}machine1\=\{ecl:ut2\}\+\+
\\[0ex]($i$; ${\it ds}$; ${\it da}$; $A$)
\-\\[0ex]$\Vdash$ ${\it es}$.\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ \=vartype($i$;"ecl") $\subseteq\rho$ ecl{-}trans{-}type(ecl{-}trans($A$))\+
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$.\+
\\[0ex]$\forall$$e$@$i$.
\\[0ex]action[[$A$ $n$]][es{-}init(${\it es}$;$e$);$e$]
\\[0ex]$\Leftrightarrow$
\\[0ex](kind($e$) $\in$ ecl{-}trans{-}ks(ecl{-}trans($A$)))
\\[0ex]\& ecl{-}trans{-}a(ecl{-}trans($A$))($n$,kind($e$),(state when $e$),val($e$),"ecl" when $e$))
\-\-\-\-
\end{tabbing}